$\forall$${\it es}$:ES, $l$:IdLnk, ${\it tg}$:Id, $A$:Type, $e$:E.
\\[0ex](kindtype(destination($l$);rcv($l$,${\it tg}$)) $\subseteq$r $A$)
\\[0ex]$\Rightarrow$ ($\uparrow$($e$ $\in_{b}$ es{-}in{-}port(${\it es}$;$l$;${\it tg}$)))
\\[0ex]$\Rightarrow$ (es{-}in{-}port(${\it es}$;$l$;${\it tg}$)($e$) = val($e$) $\in$ $A$)